﻿/*****************************************************
 * File:            MealyTCE.cs
 * Description:     ...
 * By:              Ali Khalili (khalili DOT ir AT gmail DOT com)
 * Project:         Automata Learning
 * Namespece		AIDE.TCG
 * Requirements:    
 * Change log:
 *          -21 Mat 2013:  Initial Development
 *          -31 Aug 2013: Some bug removal, adding repeating tests,add some comments
 * To Do:
 *          -
 * License:
 *****************************************************/

using System;
using System.Collections.Generic;
using SMLib.Automata.Base;
using SMLib.Automata.MM;
using SMLib.Base;
using MBT.Conformance;
//
//using EnGine.Core;
//using AIDE.Base;

namespace MBT.Conformance.TestExecution
{
    /// <summary>
    /// Mealy Machine Test Case Executor
    /// </summary>
    public class MealyTCE //: IOfflineTCE<MealyMachine.Mealy_State,MealyMachine.Mealy_Transition>
    {
        IBlackBox_MM SUT;
        MealyMachine model;

        /// <summary>
        /// Constructor
        /// </summary>
        /// <param name="SUT">the SUT</param>
        public MealyTCE(IBlackBox_MM SUT, bool deterministic=false)
        {
            this.SUT = SUT;
			if(deterministic)
			{
				MAX_NUMBER_OF_TRIES_FOR_EACH_TESTCASE=1;
				MAX_NUMBER_OF_REPEAT_FOR_EACH_TESTCASE=1;
			}
			else
			{
				MAX_NUMBER_OF_TRIES_FOR_EACH_TESTCASE = 
					MAX_NUMBER_OF_TRIES_FOR_EACH_TESTCASE_default;
				MAX_NUMBER_OF_REPEAT_FOR_EACH_TESTCASE= 
					MAX_NUMBER_OF_REPEAT_FOR_EACH_TESTCASE_default;	
			}
        }

        /// <summary>
        /// Maximum number of experimenting each test case (to falsify it). In determininistic systems, 
        /// 1 is enought!
        /// </summary>
        public static int MAX_NUMBER_OF_TRIES_FOR_EACH_TESTCASE = 1000;
		
		const int MAX_NUMBER_OF_TRIES_FOR_EACH_TESTCASE_default=1000;
        
		/// <summary>
        /// Maximum number of repeating each test case
        /// </summary>
        public static int MAX_NUMBER_OF_REPEAT_FOR_EACH_TESTCASE = 100;
		const int MAX_NUMBER_OF_REPEAT_FOR_EACH_TESTCASE_default=100;
		
        #region IOfflineTCE Members

        /// <summary>
        /// Set the mpdel
        /// </summary>
        /// <param name="model">model</param>
        public void SetModel(IDiGraph<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition> model)
        {
            if (model is MealyMachine)
            {
                this.model = (MealyMachine)model;
            }
            else
                throw new Exception("The model is not Mealy machine");
        }

        /// <summary>
        /// Verify one test case aiming to falsify it (and finding a counterexample)
        /// </summary>
        /// <param name="testCase">test case</param>
        /// <returns>counterexample (if found), null in other case</returns>
        public object FalsifyTestCase(List<MealyMachine.Mealy_Transition> testCase)
        {
            MealyMachine.Mealy_State currentState;
            bool failToVerify;
            bool verified = false;

            //* for number of -successful- repeats
            for (int t = 0; t < MAX_NUMBER_OF_REPEAT_FOR_EACH_TESTCASE; t++)
            {
                failToVerify = false;

                for (int t1 = 0; t1 < MAX_NUMBER_OF_TRIES_FOR_EACH_TESTCASE; t1++)
                {
                    currentState = (MealyMachine.Mealy_State)model[0];
                    List<PairOfSymbols> counterexample = new List<PairOfSymbols>();
                    SUT.Reset();
                    for (int i = 0; i < testCase.Count; i++)
                    {
                        ISymbol input = ((MealyMachine.Mealy_Transition)testCase[i]).inLabel;
                        ISymbol Eoutput = ((MealyMachine.Mealy_Transition)testCase[i]).outLabel;
                        ISymbol Routput = SUT.Step(input);
                        counterexample.Add(new PairOfSymbols(input, Routput));
                        if (Routput == null)
                        {
                            //Console.WriteLine("\nTrying to execute this test case:");
                            //AIDE.Utils.ListUtil.WriteList(testCase);
                            //throw new Exception("But it failed!");
                            return counterexample;
                        }
                        if (Eoutput.Equals(Routput))
                        {
                            currentState = (MealyMachine.Mealy_State)testCase[i].Destination;
                        }
                        else
                        {
                            if (!currentState.ListOfAllOutputs(input).Contains(Routput))
                            {
                                return counterexample;
                            }
                            else
                            {
                                failToVerify = true;
                                break;
                            }
                        }
                    }

                    //* we could follow the test case! So, the test case was successfull. BUT we repeat it some more time!
                    if (!failToVerify)
                    {
                        verified = true;
                        break;
                    }
                    
                }
            }

            if (!verified)
            {
                Console.Write("[");
                //AIDE.Utils.ListUtil.WriteList(testCase);
                Console.Write("]   ");
                throw new NotConclusiveVerdictException();
            }
            else
                return null;
        }

        #endregion
    }
}
